Nuprl Lemma : mon_itop_shift
13,42
postcript
pdf
g
:IMonoid,
a
,
b
:
.
(
a
b
)
(
E
:({
a
..
b
}
|
g
|),
k
:
. (
a
j
<
b
.
E
(
j
)) = (
a
+
k
j
<
b
+
k
.
E
(
j
-
k
))
|
g
|)
latex
Up
groups
1
Definitions of Statement
lb
i
<
ub
.
E
(
i
)
Definitions
lb
i
<
ub
.
E
(
i
)
Lemmas
itop
shift
origin